Termination w.r.t. Q proof of /tmp/tmpPFabFn/cade08.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

f(true, x, y, z) → f(and(gt(x, y), gt(x, z)), x, s(y), z)
f(true, x, y, z) → f(and(gt(x, y), gt(x, z)), x, y, s(z))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false

Q is empty.

↳ QTRS

  ↳ AAECC Innermost

Q restricted rewrite system:
The TRS R consists of the following rules:

f(true, x, y, z) → f(and(gt(x, y), gt(x, z)), x, s(y), z)
f(true, x, y, z) → f(and(gt(x, y), gt(x, z)), x, y, s(z))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false

Q is empty.

We have applied [19,8] to switch to innermost. The TRS R 1 is

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false

The TRS R 2 is

f(true, x, y, z) → f(and(gt(x, y), gt(x, z)), x, s(y), z)
f(true, x, y, z) → f(and(gt(x, y), gt(x, z)), x, y, s(z))

The signature Sigma is {f}

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

f(true, x, y, z) → f(and(gt(x, y), gt(x, z)), x, s(y), z)
f(true, x, y, z) → f(and(gt(x, y), gt(x, z)), x, y, s(z))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false

The set Q consists of the following terms:

f(true, x0, x1, x2)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
and(x0, true)
and(x0, false)

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

F(true, x, y, z) → GT(x, y)
F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, s(y), z)
GT(s(u), s(v)) → GT(u, v)
F(true, x, y, z) → AND(gt(x, y), gt(x, z))
F(true, x, y, z) → GT(x, z)
F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, y, s(z))

The TRS R consists of the following rules:

f(true, x, y, z) → f(and(gt(x, y), gt(x, z)), x, s(y), z)
f(true, x, y, z) → f(and(gt(x, y), gt(x, z)), x, y, s(z))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false

The set Q consists of the following terms:

f(true, x0, x1, x2)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
and(x0, true)
and(x0, false)

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

F(true, x, y, z) → GT(x, y)
F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, s(y), z)
GT(s(u), s(v)) → GT(u, v)
F(true, x, y, z) → AND(gt(x, y), gt(x, z))
F(true, x, y, z) → GT(x, z)
F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, y, s(z))

The TRS R consists of the following rules:

f(true, x, y, z) → f(and(gt(x, y), gt(x, z)), x, s(y), z)
f(true, x, y, z) → f(and(gt(x, y), gt(x, z)), x, y, s(z))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false

The set Q consists of the following terms:

f(true, x0, x1, x2)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
and(x0, true)
and(x0, false)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 3 less nodes.

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GT(s(u), s(v)) → GT(u, v)

The TRS R consists of the following rules:

f(true, x, y, z) → f(and(gt(x, y), gt(x, z)), x, s(y), z)
f(true, x, y, z) → f(and(gt(x, y), gt(x, z)), x, y, s(z))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false

The set Q consists of the following terms:

f(true, x0, x1, x2)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
and(x0, true)
and(x0, false)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GT(s(u), s(v)) → GT(u, v)

R is empty.
The set Q consists of the following terms:

f(true, x0, x1, x2)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
and(x0, true)
and(x0, false)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

f(true, x0, x1, x2)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
and(x0, true)
and(x0, false)

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GT(s(u), s(v)) → GT(u, v)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

GT(s(u), s(v)) → GT(u, v)
The graph contains the following edges 1 > 1, 2 > 2

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, s(y), z)
F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, y, s(z))

The TRS R consists of the following rules:

f(true, x, y, z) → f(and(gt(x, y), gt(x, z)), x, s(y), z)
f(true, x, y, z) → f(and(gt(x, y), gt(x, z)), x, y, s(z))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false

The set Q consists of the following terms:

f(true, x0, x1, x2)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
and(x0, true)
and(x0, false)

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, s(y), z)
F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, y, s(z))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false

The set Q consists of the following terms:

f(true, x0, x1, x2)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
and(x0, true)
and(x0, false)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

f(true, x0, x1, x2)

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ NonInfProof

Q DP problem:
The TRS P consists of the following rules:

F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, s(y), z)
F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, y, s(z))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false

The set Q consists of the following terms:

gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
and(x0, true)
and(x0, false)

We have to consider all minimal (P,Q,R)-chains.
The DP Problem is simplified using the Induction Calculus [18] with the following steps:
Note that final constraints are written in bold face.

For Pair F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, s(y), z) the following chains were created:

We consider the chain F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, s(y), z), F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, s(y), z) which results in the following constraint:
(1)    (F(and(gt(x0, x1), gt(x0, x2)), x0, s(x1), x2)=F(true, x3, x4, x5) ⇒ F(true, x3, x4, x5)≥F(and(gt(x3, x4), gt(x3, x5)), x3, s(x4), x5))

We simplified constraint (1) using rules (I), (II), (III), (VII) which results in the following new constraint:
(2)    (gt(x0, x1)=x24∧gt(x0, x2)=x25∧and(x24, x25)=true ⇒ F(true, x0, s(x1), x2)≥F(and(gt(x0, s(x1)), gt(x0, x2)), x0, s(s(x1)), x2))

We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on and(x24, x25)=true which results in the following new constraint:
(3)    (x26=true∧gt(x0, x1)=x26∧gt(x0, x2)=true ⇒ F(true, x0, s(x1), x2)≥F(and(gt(x0, s(x1)), gt(x0, x2)), x0, s(s(x1)), x2))

We simplified constraint (3) using rule (III) which results in the following new constraint:
(4)    (gt(x0, x1)=true∧gt(x0, x2)=true ⇒ F(true, x0, s(x1), x2)≥F(and(gt(x0, s(x1)), gt(x0, x2)), x0, s(s(x1)), x2))

We simplified constraint (4) using rule (V) (with possible (I) afterwards) using induction on gt(x0, x1)=true which results in the following new constraints:
(5)    (true=true∧gt(s(x29), x2)=true ⇒ F(true, s(x29), s(0), x2)≥F(and(gt(s(x29), s(0)), gt(s(x29), x2)), s(x29), s(s(0)), x2))

(6)    (gt(x30, x31)=true∧gt(s(x30), x2)=true∧(∀x32:gt(x30, x31)=true∧gt(x30, x32)=true ⇒ F(true, x30, s(x31), x32)≥F(and(gt(x30, s(x31)), gt(x30, x32)), x30, s(s(x31)), x32)) ⇒ F(true, s(x30), s(s(x31)), x2)≥F(and(gt(s(x30), s(s(x31))), gt(s(x30), x2)), s(x30), s(s(s(x31))), x2))

We simplified constraint (5) using rules (I), (II), (VII) which results in the following new constraint:
(7)    (s(x29)=x33∧gt(x33, x2)=true ⇒ F(true, s(x29), s(0), x2)≥F(and(gt(s(x29), s(0)), gt(s(x29), x2)), s(x29), s(s(0)), x2))

We simplified constraint (6) using rule (VII) which results in the following new constraint:
(8)    (gt(x30, x31)=true∧s(x30)=x43∧gt(x43, x2)=true∧(∀x32:gt(x30, x31)=true∧gt(x30, x32)=true ⇒ F(true, x30, s(x31), x32)≥F(and(gt(x30, s(x31)), gt(x30, x32)), x30, s(s(x31)), x32)) ⇒ F(true, s(x30), s(s(x31)), x2)≥F(and(gt(s(x30), s(s(x31))), gt(s(x30), x2)), s(x30), s(s(s(x31))), x2))

We simplified constraint (7) using rule (V) (with possible (I) afterwards) using induction on gt(x33, x2)=true which results in the following new constraints:
(9)    (true=true∧s(x29)=s(x35) ⇒ F(true, s(x29), s(0), 0)≥F(and(gt(s(x29), s(0)), gt(s(x29), 0)), s(x29), s(s(0)), 0))

(10)    (gt(x36, x37)=true∧s(x29)=s(x36)∧(∀x38:gt(x36, x37)=true∧s(x38)=x36 ⇒ F(true, s(x38), s(0), x37)≥F(and(gt(s(x38), s(0)), gt(s(x38), x37)), s(x38), s(s(0)), x37)) ⇒ F(true, s(x29), s(0), s(x37))≥F(and(gt(s(x29), s(0)), gt(s(x29), s(x37))), s(x29), s(s(0)), s(x37)))

We simplified constraint (9) using rules (I), (II), (IV) which results in the following new constraint:
(11)    (F(true, s(x29), s(0), 0)≥F(and(gt(s(x29), s(0)), gt(s(x29), 0)), s(x29), s(s(0)), 0))

We simplified constraint (10) using rules (I), (II), (III), (IV) which results in the following new constraint:
(12)    (gt(x36, x37)=true ⇒ F(true, s(x36), s(0), s(x37))≥F(and(gt(s(x36), s(0)), gt(s(x36), s(x37))), s(x36), s(s(0)), s(x37)))

We simplified constraint (12) using rule (V) (with possible (I) afterwards) using induction on gt(x36, x37)=true which results in the following new constraints:
(13)    (true=true ⇒ F(true, s(s(x40)), s(0), s(0))≥F(and(gt(s(s(x40)), s(0)), gt(s(s(x40)), s(0))), s(s(x40)), s(s(0)), s(0)))

(14)    (gt(x41, x42)=true∧(gt(x41, x42)=true ⇒ F(true, s(x41), s(0), s(x42))≥F(and(gt(s(x41), s(0)), gt(s(x41), s(x42))), s(x41), s(s(0)), s(x42))) ⇒ F(true, s(s(x41)), s(0), s(s(x42)))≥F(and(gt(s(s(x41)), s(0)), gt(s(s(x41)), s(s(x42)))), s(s(x41)), s(s(0)), s(s(x42))))

We simplified constraint (13) using rules (I), (II) which results in the following new constraint:
(15)    (F(true, s(s(x40)), s(0), s(0))≥F(and(gt(s(s(x40)), s(0)), gt(s(s(x40)), s(0))), s(s(x40)), s(s(0)), s(0)))

We simplified constraint (14) using rule (VI) where we applied the induction hypothesis (gt(x41, x42)=true ⇒ F(true, s(x41), s(0), s(x42))≥F(and(gt(s(x41), s(0)), gt(s(x41), s(x42))), s(x41), s(s(0)), s(x42))) with σ = [ ] which results in the following new constraint:
(16)    (F(true, s(x41), s(0), s(x42))≥F(and(gt(s(x41), s(0)), gt(s(x41), s(x42))), s(x41), s(s(0)), s(x42)) ⇒ F(true, s(s(x41)), s(0), s(s(x42)))≥F(and(gt(s(s(x41)), s(0)), gt(s(s(x41)), s(s(x42)))), s(s(x41)), s(s(0)), s(s(x42))))

We simplified constraint (8) using rule (V) (with possible (I) afterwards) using induction on gt(x43, x2)=true which results in the following new constraints:
(17)    (true=true∧gt(x30, x31)=true∧s(x30)=s(x45)∧(∀x32:gt(x30, x31)=true∧gt(x30, x32)=true ⇒ F(true, x30, s(x31), x32)≥F(and(gt(x30, s(x31)), gt(x30, x32)), x30, s(s(x31)), x32)) ⇒ F(true, s(x30), s(s(x31)), 0)≥F(and(gt(s(x30), s(s(x31))), gt(s(x30), 0)), s(x30), s(s(s(x31))), 0))

(18)    (gt(x46, x47)=true∧gt(x30, x31)=true∧s(x30)=s(x46)∧(∀x32:gt(x30, x31)=true∧gt(x30, x32)=true ⇒ F(true, x30, s(x31), x32)≥F(and(gt(x30, s(x31)), gt(x30, x32)), x30, s(s(x31)), x32))∧(∀x48,x49,x50:gt(x46, x47)=true∧gt(x48, x49)=true∧s(x48)=x46∧(∀x50:gt(x48, x49)=true∧gt(x48, x50)=true ⇒ F(true, x48, s(x49), x50)≥F(and(gt(x48, s(x49)), gt(x48, x50)), x48, s(s(x49)), x50)) ⇒ F(true, s(x48), s(s(x49)), x47)≥F(and(gt(s(x48), s(s(x49))), gt(s(x48), x47)), s(x48), s(s(s(x49))), x47)) ⇒ F(true, s(x30), s(s(x31)), s(x47))≥F(and(gt(s(x30), s(s(x31))), gt(s(x30), s(x47))), s(x30), s(s(s(x31))), s(x47)))

We simplified constraint (17) using rules (I), (II), (IV) which results in the following new constraint:
(19)    (gt(x30, x31)=true ⇒ F(true, s(x30), s(s(x31)), 0)≥F(and(gt(s(x30), s(s(x31))), gt(s(x30), 0)), s(x30), s(s(s(x31))), 0))

We simplified constraint (18) using rules (I), (II), (III) which results in the following new constraint:
(20)    (gt(x46, x47)=true∧gt(x46, x31)=true∧(∀x32:gt(x46, x31)=true∧gt(x46, x32)=true ⇒ F(true, x46, s(x31), x32)≥F(and(gt(x46, s(x31)), gt(x46, x32)), x46, s(s(x31)), x32))∧(∀x48,x49,x50:gt(x46, x47)=true∧gt(x48, x49)=true∧s(x48)=x46∧(∀x50:gt(x48, x49)=true∧gt(x48, x50)=true ⇒ F(true, x48, s(x49), x50)≥F(and(gt(x48, s(x49)), gt(x48, x50)), x48, s(s(x49)), x50)) ⇒ F(true, s(x48), s(s(x49)), x47)≥F(and(gt(s(x48), s(s(x49))), gt(s(x48), x47)), s(x48), s(s(s(x49))), x47)) ⇒ F(true, s(x46), s(s(x31)), s(x47))≥F(and(gt(s(x46), s(s(x31))), gt(s(x46), s(x47))), s(x46), s(s(s(x31))), s(x47)))

We simplified constraint (19) using rule (V) (with possible (I) afterwards) using induction on gt(x30, x31)=true which results in the following new constraints:
(21)    (true=true ⇒ F(true, s(s(x52)), s(s(0)), 0)≥F(and(gt(s(s(x52)), s(s(0))), gt(s(s(x52)), 0)), s(s(x52)), s(s(s(0))), 0))

(22)    (gt(x53, x54)=true∧(gt(x53, x54)=true ⇒ F(true, s(x53), s(s(x54)), 0)≥F(and(gt(s(x53), s(s(x54))), gt(s(x53), 0)), s(x53), s(s(s(x54))), 0)) ⇒ F(true, s(s(x53)), s(s(s(x54))), 0)≥F(and(gt(s(s(x53)), s(s(s(x54)))), gt(s(s(x53)), 0)), s(s(x53)), s(s(s(s(x54)))), 0))

We simplified constraint (21) using rules (I), (II) which results in the following new constraint:
(23)    (F(true, s(s(x52)), s(s(0)), 0)≥F(and(gt(s(s(x52)), s(s(0))), gt(s(s(x52)), 0)), s(s(x52)), s(s(s(0))), 0))

We simplified constraint (22) using rule (VI) where we applied the induction hypothesis (gt(x53, x54)=true ⇒ F(true, s(x53), s(s(x54)), 0)≥F(and(gt(s(x53), s(s(x54))), gt(s(x53), 0)), s(x53), s(s(s(x54))), 0)) with σ = [ ] which results in the following new constraint:
(24)    (F(true, s(x53), s(s(x54)), 0)≥F(and(gt(s(x53), s(s(x54))), gt(s(x53), 0)), s(x53), s(s(s(x54))), 0) ⇒ F(true, s(s(x53)), s(s(s(x54))), 0)≥F(and(gt(s(s(x53)), s(s(s(x54)))), gt(s(s(x53)), 0)), s(s(x53)), s(s(s(s(x54)))), 0))

We simplified constraint (20) using rule (VI) where we applied the induction hypothesis (∀x32:gt(x46, x31)=true∧gt(x46, x32)=true ⇒ F(true, x46, s(x31), x32)≥F(and(gt(x46, s(x31)), gt(x46, x32)), x46, s(s(x31)), x32)) with σ = [x32 / x47] which results in the following new constraint:
(25)    (F(true, x46, s(x31), x47)≥F(and(gt(x46, s(x31)), gt(x46, x47)), x46, s(s(x31)), x47)∧(∀x48,x49,x50:gt(x46, x47)=true∧gt(x48, x49)=true∧s(x48)=x46∧(∀x50:gt(x48, x49)=true∧gt(x48, x50)=true ⇒ F(true, x48, s(x49), x50)≥F(and(gt(x48, s(x49)), gt(x48, x50)), x48, s(s(x49)), x50)) ⇒ F(true, s(x48), s(s(x49)), x47)≥F(and(gt(s(x48), s(s(x49))), gt(s(x48), x47)), s(x48), s(s(s(x49))), x47)) ⇒ F(true, s(x46), s(s(x31)), s(x47))≥F(and(gt(s(x46), s(s(x31))), gt(s(x46), s(x47))), s(x46), s(s(s(x31))), s(x47)))

We simplified constraint (25) using rule (IV) which results in the following new constraint:
(26)    (F(true, x46, s(x31), x47)≥F(and(gt(x46, s(x31)), gt(x46, x47)), x46, s(s(x31)), x47) ⇒ F(true, s(x46), s(s(x31)), s(x47))≥F(and(gt(s(x46), s(s(x31))), gt(s(x46), s(x47))), s(x46), s(s(s(x31))), s(x47)))
We consider the chain F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, y, s(z)), F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, s(y), z) which results in the following constraint:
(27)    (F(and(gt(x6, x7), gt(x6, x8)), x6, x7, s(x8))=F(true, x9, x10, x11) ⇒ F(true, x9, x10, x11)≥F(and(gt(x9, x10), gt(x9, x11)), x9, s(x10), x11))

We simplified constraint (27) using rules (I), (II), (III), (VII) which results in the following new constraint:
(28)    (gt(x6, x7)=x55∧gt(x6, x8)=x56∧and(x55, x56)=true ⇒ F(true, x6, x7, s(x8))≥F(and(gt(x6, x7), gt(x6, s(x8))), x6, s(x7), s(x8)))

We simplified constraint (28) using rule (V) (with possible (I) afterwards) using induction on and(x55, x56)=true which results in the following new constraint:
(29)    (x57=true∧gt(x6, x7)=x57∧gt(x6, x8)=true ⇒ F(true, x6, x7, s(x8))≥F(and(gt(x6, x7), gt(x6, s(x8))), x6, s(x7), s(x8)))

We simplified constraint (29) using rule (III) which results in the following new constraint:
(30)    (gt(x6, x7)=true∧gt(x6, x8)=true ⇒ F(true, x6, x7, s(x8))≥F(and(gt(x6, x7), gt(x6, s(x8))), x6, s(x7), s(x8)))

We simplified constraint (30) using rule (V) (with possible (I) afterwards) using induction on gt(x6, x7)=true which results in the following new constraints:
(31)    (true=true∧gt(s(x60), x8)=true ⇒ F(true, s(x60), 0, s(x8))≥F(and(gt(s(x60), 0), gt(s(x60), s(x8))), s(x60), s(0), s(x8)))

(32)    (gt(x61, x62)=true∧gt(s(x61), x8)=true∧(∀x63:gt(x61, x62)=true∧gt(x61, x63)=true ⇒ F(true, x61, x62, s(x63))≥F(and(gt(x61, x62), gt(x61, s(x63))), x61, s(x62), s(x63))) ⇒ F(true, s(x61), s(x62), s(x8))≥F(and(gt(s(x61), s(x62)), gt(s(x61), s(x8))), s(x61), s(s(x62)), s(x8)))

We simplified constraint (31) using rules (I), (II), (VII) which results in the following new constraint:
(33)    (s(x60)=x64∧gt(x64, x8)=true ⇒ F(true, s(x60), 0, s(x8))≥F(and(gt(s(x60), 0), gt(s(x60), s(x8))), s(x60), s(0), s(x8)))

We simplified constraint (32) using rule (VII) which results in the following new constraint:
(34)    (gt(x61, x62)=true∧s(x61)=x74∧gt(x74, x8)=true∧(∀x63:gt(x61, x62)=true∧gt(x61, x63)=true ⇒ F(true, x61, x62, s(x63))≥F(and(gt(x61, x62), gt(x61, s(x63))), x61, s(x62), s(x63))) ⇒ F(true, s(x61), s(x62), s(x8))≥F(and(gt(s(x61), s(x62)), gt(s(x61), s(x8))), s(x61), s(s(x62)), s(x8)))

We simplified constraint (33) using rule (V) (with possible (I) afterwards) using induction on gt(x64, x8)=true which results in the following new constraints:
(35)    (true=true∧s(x60)=s(x66) ⇒ F(true, s(x60), 0, s(0))≥F(and(gt(s(x60), 0), gt(s(x60), s(0))), s(x60), s(0), s(0)))

(36)    (gt(x67, x68)=true∧s(x60)=s(x67)∧(∀x69:gt(x67, x68)=true∧s(x69)=x67 ⇒ F(true, s(x69), 0, s(x68))≥F(and(gt(s(x69), 0), gt(s(x69), s(x68))), s(x69), s(0), s(x68))) ⇒ F(true, s(x60), 0, s(s(x68)))≥F(and(gt(s(x60), 0), gt(s(x60), s(s(x68)))), s(x60), s(0), s(s(x68))))

We simplified constraint (35) using rules (I), (II), (IV) which results in the following new constraint:
(37)    (F(true, s(x60), 0, s(0))≥F(and(gt(s(x60), 0), gt(s(x60), s(0))), s(x60), s(0), s(0)))

We simplified constraint (36) using rules (I), (II), (III), (IV) which results in the following new constraint:
(38)    (gt(x67, x68)=true ⇒ F(true, s(x67), 0, s(s(x68)))≥F(and(gt(s(x67), 0), gt(s(x67), s(s(x68)))), s(x67), s(0), s(s(x68))))

We simplified constraint (38) using rule (V) (with possible (I) afterwards) using induction on gt(x67, x68)=true which results in the following new constraints:
(39)    (true=true ⇒ F(true, s(s(x71)), 0, s(s(0)))≥F(and(gt(s(s(x71)), 0), gt(s(s(x71)), s(s(0)))), s(s(x71)), s(0), s(s(0))))

(40)    (gt(x72, x73)=true∧(gt(x72, x73)=true ⇒ F(true, s(x72), 0, s(s(x73)))≥F(and(gt(s(x72), 0), gt(s(x72), s(s(x73)))), s(x72), s(0), s(s(x73)))) ⇒ F(true, s(s(x72)), 0, s(s(s(x73))))≥F(and(gt(s(s(x72)), 0), gt(s(s(x72)), s(s(s(x73))))), s(s(x72)), s(0), s(s(s(x73)))))

We simplified constraint (39) using rules (I), (II) which results in the following new constraint:
(41)    (F(true, s(s(x71)), 0, s(s(0)))≥F(and(gt(s(s(x71)), 0), gt(s(s(x71)), s(s(0)))), s(s(x71)), s(0), s(s(0))))

We simplified constraint (40) using rule (VI) where we applied the induction hypothesis (gt(x72, x73)=true ⇒ F(true, s(x72), 0, s(s(x73)))≥F(and(gt(s(x72), 0), gt(s(x72), s(s(x73)))), s(x72), s(0), s(s(x73)))) with σ = [ ] which results in the following new constraint:
(42)    (F(true, s(x72), 0, s(s(x73)))≥F(and(gt(s(x72), 0), gt(s(x72), s(s(x73)))), s(x72), s(0), s(s(x73))) ⇒ F(true, s(s(x72)), 0, s(s(s(x73))))≥F(and(gt(s(s(x72)), 0), gt(s(s(x72)), s(s(s(x73))))), s(s(x72)), s(0), s(s(s(x73)))))

We simplified constraint (34) using rule (V) (with possible (I) afterwards) using induction on gt(x74, x8)=true which results in the following new constraints:
(43)    (true=true∧gt(x61, x62)=true∧s(x61)=s(x76)∧(∀x63:gt(x61, x62)=true∧gt(x61, x63)=true ⇒ F(true, x61, x62, s(x63))≥F(and(gt(x61, x62), gt(x61, s(x63))), x61, s(x62), s(x63))) ⇒ F(true, s(x61), s(x62), s(0))≥F(and(gt(s(x61), s(x62)), gt(s(x61), s(0))), s(x61), s(s(x62)), s(0)))

(44)    (gt(x77, x78)=true∧gt(x61, x62)=true∧s(x61)=s(x77)∧(∀x63:gt(x61, x62)=true∧gt(x61, x63)=true ⇒ F(true, x61, x62, s(x63))≥F(and(gt(x61, x62), gt(x61, s(x63))), x61, s(x62), s(x63)))∧(∀x79,x80,x81:gt(x77, x78)=true∧gt(x79, x80)=true∧s(x79)=x77∧(∀x81:gt(x79, x80)=true∧gt(x79, x81)=true ⇒ F(true, x79, x80, s(x81))≥F(and(gt(x79, x80), gt(x79, s(x81))), x79, s(x80), s(x81))) ⇒ F(true, s(x79), s(x80), s(x78))≥F(and(gt(s(x79), s(x80)), gt(s(x79), s(x78))), s(x79), s(s(x80)), s(x78))) ⇒ F(true, s(x61), s(x62), s(s(x78)))≥F(and(gt(s(x61), s(x62)), gt(s(x61), s(s(x78)))), s(x61), s(s(x62)), s(s(x78))))

We simplified constraint (43) using rules (I), (II), (IV) which results in the following new constraint:
(45)    (gt(x61, x62)=true ⇒ F(true, s(x61), s(x62), s(0))≥F(and(gt(s(x61), s(x62)), gt(s(x61), s(0))), s(x61), s(s(x62)), s(0)))

We simplified constraint (44) using rules (I), (II), (III) which results in the following new constraint:
(46)    (gt(x77, x78)=true∧gt(x77, x62)=true∧(∀x63:gt(x77, x62)=true∧gt(x77, x63)=true ⇒ F(true, x77, x62, s(x63))≥F(and(gt(x77, x62), gt(x77, s(x63))), x77, s(x62), s(x63)))∧(∀x79,x80,x81:gt(x77, x78)=true∧gt(x79, x80)=true∧s(x79)=x77∧(∀x81:gt(x79, x80)=true∧gt(x79, x81)=true ⇒ F(true, x79, x80, s(x81))≥F(and(gt(x79, x80), gt(x79, s(x81))), x79, s(x80), s(x81))) ⇒ F(true, s(x79), s(x80), s(x78))≥F(and(gt(s(x79), s(x80)), gt(s(x79), s(x78))), s(x79), s(s(x80)), s(x78))) ⇒ F(true, s(x77), s(x62), s(s(x78)))≥F(and(gt(s(x77), s(x62)), gt(s(x77), s(s(x78)))), s(x77), s(s(x62)), s(s(x78))))

We simplified constraint (45) using rule (V) (with possible (I) afterwards) using induction on gt(x61, x62)=true which results in the following new constraints:
(47)    (true=true ⇒ F(true, s(s(x83)), s(0), s(0))≥F(and(gt(s(s(x83)), s(0)), gt(s(s(x83)), s(0))), s(s(x83)), s(s(0)), s(0)))

(48)    (gt(x84, x85)=true∧(gt(x84, x85)=true ⇒ F(true, s(x84), s(x85), s(0))≥F(and(gt(s(x84), s(x85)), gt(s(x84), s(0))), s(x84), s(s(x85)), s(0))) ⇒ F(true, s(s(x84)), s(s(x85)), s(0))≥F(and(gt(s(s(x84)), s(s(x85))), gt(s(s(x84)), s(0))), s(s(x84)), s(s(s(x85))), s(0)))

We simplified constraint (47) using rules (I), (II) which results in the following new constraint:
(49)    (F(true, s(s(x83)), s(0), s(0))≥F(and(gt(s(s(x83)), s(0)), gt(s(s(x83)), s(0))), s(s(x83)), s(s(0)), s(0)))

We simplified constraint (48) using rule (VI) where we applied the induction hypothesis (gt(x84, x85)=true ⇒ F(true, s(x84), s(x85), s(0))≥F(and(gt(s(x84), s(x85)), gt(s(x84), s(0))), s(x84), s(s(x85)), s(0))) with σ = [ ] which results in the following new constraint:
(50)    (F(true, s(x84), s(x85), s(0))≥F(and(gt(s(x84), s(x85)), gt(s(x84), s(0))), s(x84), s(s(x85)), s(0)) ⇒ F(true, s(s(x84)), s(s(x85)), s(0))≥F(and(gt(s(s(x84)), s(s(x85))), gt(s(s(x84)), s(0))), s(s(x84)), s(s(s(x85))), s(0)))

We simplified constraint (46) using rule (VI) where we applied the induction hypothesis (∀x63:gt(x77, x62)=true∧gt(x77, x63)=true ⇒ F(true, x77, x62, s(x63))≥F(and(gt(x77, x62), gt(x77, s(x63))), x77, s(x62), s(x63))) with σ = [x63 / x78] which results in the following new constraint:
(51)    (F(true, x77, x62, s(x78))≥F(and(gt(x77, x62), gt(x77, s(x78))), x77, s(x62), s(x78))∧(∀x79,x80,x81:gt(x77, x78)=true∧gt(x79, x80)=true∧s(x79)=x77∧(∀x81:gt(x79, x80)=true∧gt(x79, x81)=true ⇒ F(true, x79, x80, s(x81))≥F(and(gt(x79, x80), gt(x79, s(x81))), x79, s(x80), s(x81))) ⇒ F(true, s(x79), s(x80), s(x78))≥F(and(gt(s(x79), s(x80)), gt(s(x79), s(x78))), s(x79), s(s(x80)), s(x78))) ⇒ F(true, s(x77), s(x62), s(s(x78)))≥F(and(gt(s(x77), s(x62)), gt(s(x77), s(s(x78)))), s(x77), s(s(x62)), s(s(x78))))

We simplified constraint (51) using rule (IV) which results in the following new constraint:
(52)    (F(true, x77, x62, s(x78))≥F(and(gt(x77, x62), gt(x77, s(x78))), x77, s(x62), s(x78)) ⇒ F(true, s(x77), s(x62), s(s(x78)))≥F(and(gt(s(x77), s(x62)), gt(s(x77), s(s(x78)))), s(x77), s(s(x62)), s(s(x78))))

For Pair F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, y, s(z)) the following chains were created:

We consider the chain F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, s(y), z), F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, y, s(z)) which results in the following constraint:
(53)    (F(and(gt(x12, x13), gt(x12, x14)), x12, s(x13), x14)=F(true, x15, x16, x17) ⇒ F(true, x15, x16, x17)≥F(and(gt(x15, x16), gt(x15, x17)), x15, x16, s(x17)))

We simplified constraint (53) using rules (I), (II), (III), (VII) which results in the following new constraint:
(54)    (gt(x12, x13)=x86∧gt(x12, x14)=x87∧and(x86, x87)=true ⇒ F(true, x12, s(x13), x14)≥F(and(gt(x12, s(x13)), gt(x12, x14)), x12, s(x13), s(x14)))

We simplified constraint (54) using rule (V) (with possible (I) afterwards) using induction on and(x86, x87)=true which results in the following new constraint:
(55)    (x88=true∧gt(x12, x13)=x88∧gt(x12, x14)=true ⇒ F(true, x12, s(x13), x14)≥F(and(gt(x12, s(x13)), gt(x12, x14)), x12, s(x13), s(x14)))

We simplified constraint (55) using rule (III) which results in the following new constraint:
(56)    (gt(x12, x13)=true∧gt(x12, x14)=true ⇒ F(true, x12, s(x13), x14)≥F(and(gt(x12, s(x13)), gt(x12, x14)), x12, s(x13), s(x14)))

We simplified constraint (56) using rule (V) (with possible (I) afterwards) using induction on gt(x12, x13)=true which results in the following new constraints:
(57)    (true=true∧gt(s(x91), x14)=true ⇒ F(true, s(x91), s(0), x14)≥F(and(gt(s(x91), s(0)), gt(s(x91), x14)), s(x91), s(0), s(x14)))

(58)    (gt(x92, x93)=true∧gt(s(x92), x14)=true∧(∀x94:gt(x92, x93)=true∧gt(x92, x94)=true ⇒ F(true, x92, s(x93), x94)≥F(and(gt(x92, s(x93)), gt(x92, x94)), x92, s(x93), s(x94))) ⇒ F(true, s(x92), s(s(x93)), x14)≥F(and(gt(s(x92), s(s(x93))), gt(s(x92), x14)), s(x92), s(s(x93)), s(x14)))

We simplified constraint (57) using rules (I), (II), (VII) which results in the following new constraint:
(59)    (s(x91)=x95∧gt(x95, x14)=true ⇒ F(true, s(x91), s(0), x14)≥F(and(gt(s(x91), s(0)), gt(s(x91), x14)), s(x91), s(0), s(x14)))

We simplified constraint (58) using rule (VII) which results in the following new constraint:
(60)    (gt(x92, x93)=true∧s(x92)=x105∧gt(x105, x14)=true∧(∀x94:gt(x92, x93)=true∧gt(x92, x94)=true ⇒ F(true, x92, s(x93), x94)≥F(and(gt(x92, s(x93)), gt(x92, x94)), x92, s(x93), s(x94))) ⇒ F(true, s(x92), s(s(x93)), x14)≥F(and(gt(s(x92), s(s(x93))), gt(s(x92), x14)), s(x92), s(s(x93)), s(x14)))

We simplified constraint (59) using rule (V) (with possible (I) afterwards) using induction on gt(x95, x14)=true which results in the following new constraints:
(61)    (true=true∧s(x91)=s(x97) ⇒ F(true, s(x91), s(0), 0)≥F(and(gt(s(x91), s(0)), gt(s(x91), 0)), s(x91), s(0), s(0)))

(62)    (gt(x98, x99)=true∧s(x91)=s(x98)∧(∀x100:gt(x98, x99)=true∧s(x100)=x98 ⇒ F(true, s(x100), s(0), x99)≥F(and(gt(s(x100), s(0)), gt(s(x100), x99)), s(x100), s(0), s(x99))) ⇒ F(true, s(x91), s(0), s(x99))≥F(and(gt(s(x91), s(0)), gt(s(x91), s(x99))), s(x91), s(0), s(s(x99))))

We simplified constraint (61) using rules (I), (II), (IV) which results in the following new constraint:
(63)    (F(true, s(x91), s(0), 0)≥F(and(gt(s(x91), s(0)), gt(s(x91), 0)), s(x91), s(0), s(0)))

We simplified constraint (62) using rules (I), (II), (III), (IV) which results in the following new constraint:
(64)    (gt(x98, x99)=true ⇒ F(true, s(x98), s(0), s(x99))≥F(and(gt(s(x98), s(0)), gt(s(x98), s(x99))), s(x98), s(0), s(s(x99))))

We simplified constraint (64) using rule (V) (with possible (I) afterwards) using induction on gt(x98, x99)=true which results in the following new constraints:
(65)    (true=true ⇒ F(true, s(s(x102)), s(0), s(0))≥F(and(gt(s(s(x102)), s(0)), gt(s(s(x102)), s(0))), s(s(x102)), s(0), s(s(0))))

(66)    (gt(x103, x104)=true∧(gt(x103, x104)=true ⇒ F(true, s(x103), s(0), s(x104))≥F(and(gt(s(x103), s(0)), gt(s(x103), s(x104))), s(x103), s(0), s(s(x104)))) ⇒ F(true, s(s(x103)), s(0), s(s(x104)))≥F(and(gt(s(s(x103)), s(0)), gt(s(s(x103)), s(s(x104)))), s(s(x103)), s(0), s(s(s(x104)))))

We simplified constraint (65) using rules (I), (II) which results in the following new constraint:
(67)    (F(true, s(s(x102)), s(0), s(0))≥F(and(gt(s(s(x102)), s(0)), gt(s(s(x102)), s(0))), s(s(x102)), s(0), s(s(0))))

We simplified constraint (66) using rule (VI) where we applied the induction hypothesis (gt(x103, x104)=true ⇒ F(true, s(x103), s(0), s(x104))≥F(and(gt(s(x103), s(0)), gt(s(x103), s(x104))), s(x103), s(0), s(s(x104)))) with σ = [ ] which results in the following new constraint:
(68)    (F(true, s(x103), s(0), s(x104))≥F(and(gt(s(x103), s(0)), gt(s(x103), s(x104))), s(x103), s(0), s(s(x104))) ⇒ F(true, s(s(x103)), s(0), s(s(x104)))≥F(and(gt(s(s(x103)), s(0)), gt(s(s(x103)), s(s(x104)))), s(s(x103)), s(0), s(s(s(x104)))))

We simplified constraint (60) using rule (V) (with possible (I) afterwards) using induction on gt(x105, x14)=true which results in the following new constraints:
(69)    (true=true∧gt(x92, x93)=true∧s(x92)=s(x107)∧(∀x94:gt(x92, x93)=true∧gt(x92, x94)=true ⇒ F(true, x92, s(x93), x94)≥F(and(gt(x92, s(x93)), gt(x92, x94)), x92, s(x93), s(x94))) ⇒ F(true, s(x92), s(s(x93)), 0)≥F(and(gt(s(x92), s(s(x93))), gt(s(x92), 0)), s(x92), s(s(x93)), s(0)))

(70)    (gt(x108, x109)=true∧gt(x92, x93)=true∧s(x92)=s(x108)∧(∀x94:gt(x92, x93)=true∧gt(x92, x94)=true ⇒ F(true, x92, s(x93), x94)≥F(and(gt(x92, s(x93)), gt(x92, x94)), x92, s(x93), s(x94)))∧(∀x110,x111,x112:gt(x108, x109)=true∧gt(x110, x111)=true∧s(x110)=x108∧(∀x112:gt(x110, x111)=true∧gt(x110, x112)=true ⇒ F(true, x110, s(x111), x112)≥F(and(gt(x110, s(x111)), gt(x110, x112)), x110, s(x111), s(x112))) ⇒ F(true, s(x110), s(s(x111)), x109)≥F(and(gt(s(x110), s(s(x111))), gt(s(x110), x109)), s(x110), s(s(x111)), s(x109))) ⇒ F(true, s(x92), s(s(x93)), s(x109))≥F(and(gt(s(x92), s(s(x93))), gt(s(x92), s(x109))), s(x92), s(s(x93)), s(s(x109))))

We simplified constraint (69) using rules (I), (II), (IV) which results in the following new constraint:
(71)    (gt(x92, x93)=true ⇒ F(true, s(x92), s(s(x93)), 0)≥F(and(gt(s(x92), s(s(x93))), gt(s(x92), 0)), s(x92), s(s(x93)), s(0)))

We simplified constraint (70) using rules (I), (II), (III) which results in the following new constraint:
(72)    (gt(x108, x109)=true∧gt(x108, x93)=true∧(∀x94:gt(x108, x93)=true∧gt(x108, x94)=true ⇒ F(true, x108, s(x93), x94)≥F(and(gt(x108, s(x93)), gt(x108, x94)), x108, s(x93), s(x94)))∧(∀x110,x111,x112:gt(x108, x109)=true∧gt(x110, x111)=true∧s(x110)=x108∧(∀x112:gt(x110, x111)=true∧gt(x110, x112)=true ⇒ F(true, x110, s(x111), x112)≥F(and(gt(x110, s(x111)), gt(x110, x112)), x110, s(x111), s(x112))) ⇒ F(true, s(x110), s(s(x111)), x109)≥F(and(gt(s(x110), s(s(x111))), gt(s(x110), x109)), s(x110), s(s(x111)), s(x109))) ⇒ F(true, s(x108), s(s(x93)), s(x109))≥F(and(gt(s(x108), s(s(x93))), gt(s(x108), s(x109))), s(x108), s(s(x93)), s(s(x109))))

We simplified constraint (71) using rule (V) (with possible (I) afterwards) using induction on gt(x92, x93)=true which results in the following new constraints:
(73)    (true=true ⇒ F(true, s(s(x114)), s(s(0)), 0)≥F(and(gt(s(s(x114)), s(s(0))), gt(s(s(x114)), 0)), s(s(x114)), s(s(0)), s(0)))

(74)    (gt(x115, x116)=true∧(gt(x115, x116)=true ⇒ F(true, s(x115), s(s(x116)), 0)≥F(and(gt(s(x115), s(s(x116))), gt(s(x115), 0)), s(x115), s(s(x116)), s(0))) ⇒ F(true, s(s(x115)), s(s(s(x116))), 0)≥F(and(gt(s(s(x115)), s(s(s(x116)))), gt(s(s(x115)), 0)), s(s(x115)), s(s(s(x116))), s(0)))

We simplified constraint (73) using rules (I), (II) which results in the following new constraint:
(75)    (F(true, s(s(x114)), s(s(0)), 0)≥F(and(gt(s(s(x114)), s(s(0))), gt(s(s(x114)), 0)), s(s(x114)), s(s(0)), s(0)))

We simplified constraint (74) using rule (VI) where we applied the induction hypothesis (gt(x115, x116)=true ⇒ F(true, s(x115), s(s(x116)), 0)≥F(and(gt(s(x115), s(s(x116))), gt(s(x115), 0)), s(x115), s(s(x116)), s(0))) with σ = [ ] which results in the following new constraint:
(76)    (F(true, s(x115), s(s(x116)), 0)≥F(and(gt(s(x115), s(s(x116))), gt(s(x115), 0)), s(x115), s(s(x116)), s(0)) ⇒ F(true, s(s(x115)), s(s(s(x116))), 0)≥F(and(gt(s(s(x115)), s(s(s(x116)))), gt(s(s(x115)), 0)), s(s(x115)), s(s(s(x116))), s(0)))

We simplified constraint (72) using rule (VI) where we applied the induction hypothesis (∀x94:gt(x108, x93)=true∧gt(x108, x94)=true ⇒ F(true, x108, s(x93), x94)≥F(and(gt(x108, s(x93)), gt(x108, x94)), x108, s(x93), s(x94))) with σ = [x94 / x109] which results in the following new constraint:
(77)    (F(true, x108, s(x93), x109)≥F(and(gt(x108, s(x93)), gt(x108, x109)), x108, s(x93), s(x109))∧(∀x110,x111,x112:gt(x108, x109)=true∧gt(x110, x111)=true∧s(x110)=x108∧(∀x112:gt(x110, x111)=true∧gt(x110, x112)=true ⇒ F(true, x110, s(x111), x112)≥F(and(gt(x110, s(x111)), gt(x110, x112)), x110, s(x111), s(x112))) ⇒ F(true, s(x110), s(s(x111)), x109)≥F(and(gt(s(x110), s(s(x111))), gt(s(x110), x109)), s(x110), s(s(x111)), s(x109))) ⇒ F(true, s(x108), s(s(x93)), s(x109))≥F(and(gt(s(x108), s(s(x93))), gt(s(x108), s(x109))), s(x108), s(s(x93)), s(s(x109))))

We simplified constraint (77) using rule (IV) which results in the following new constraint:
(78)    (F(true, x108, s(x93), x109)≥F(and(gt(x108, s(x93)), gt(x108, x109)), x108, s(x93), s(x109)) ⇒ F(true, s(x108), s(s(x93)), s(x109))≥F(and(gt(s(x108), s(s(x93))), gt(s(x108), s(x109))), s(x108), s(s(x93)), s(s(x109))))
We consider the chain F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, y, s(z)), F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, y, s(z)) which results in the following constraint:
(79)    (F(and(gt(x18, x19), gt(x18, x20)), x18, x19, s(x20))=F(true, x21, x22, x23) ⇒ F(true, x21, x22, x23)≥F(and(gt(x21, x22), gt(x21, x23)), x21, x22, s(x23)))

We simplified constraint (79) using rules (I), (II), (III), (VII) which results in the following new constraint:
(80)    (gt(x18, x19)=x117∧gt(x18, x20)=x118∧and(x117, x118)=true ⇒ F(true, x18, x19, s(x20))≥F(and(gt(x18, x19), gt(x18, s(x20))), x18, x19, s(s(x20))))

We simplified constraint (80) using rule (V) (with possible (I) afterwards) using induction on and(x117, x118)=true which results in the following new constraint:
(81)    (x119=true∧gt(x18, x19)=x119∧gt(x18, x20)=true ⇒ F(true, x18, x19, s(x20))≥F(and(gt(x18, x19), gt(x18, s(x20))), x18, x19, s(s(x20))))

We simplified constraint (81) using rule (III) which results in the following new constraint:
(82)    (gt(x18, x19)=true∧gt(x18, x20)=true ⇒ F(true, x18, x19, s(x20))≥F(and(gt(x18, x19), gt(x18, s(x20))), x18, x19, s(s(x20))))

We simplified constraint (82) using rule (V) (with possible (I) afterwards) using induction on gt(x18, x19)=true which results in the following new constraints:
(83)    (true=true∧gt(s(x122), x20)=true ⇒ F(true, s(x122), 0, s(x20))≥F(and(gt(s(x122), 0), gt(s(x122), s(x20))), s(x122), 0, s(s(x20))))

(84)    (gt(x123, x124)=true∧gt(s(x123), x20)=true∧(∀x125:gt(x123, x124)=true∧gt(x123, x125)=true ⇒ F(true, x123, x124, s(x125))≥F(and(gt(x123, x124), gt(x123, s(x125))), x123, x124, s(s(x125)))) ⇒ F(true, s(x123), s(x124), s(x20))≥F(and(gt(s(x123), s(x124)), gt(s(x123), s(x20))), s(x123), s(x124), s(s(x20))))

We simplified constraint (83) using rules (I), (II), (VII) which results in the following new constraint:
(85)    (s(x122)=x126∧gt(x126, x20)=true ⇒ F(true, s(x122), 0, s(x20))≥F(and(gt(s(x122), 0), gt(s(x122), s(x20))), s(x122), 0, s(s(x20))))

We simplified constraint (84) using rule (VII) which results in the following new constraint:
(86)    (gt(x123, x124)=true∧s(x123)=x136∧gt(x136, x20)=true∧(∀x125:gt(x123, x124)=true∧gt(x123, x125)=true ⇒ F(true, x123, x124, s(x125))≥F(and(gt(x123, x124), gt(x123, s(x125))), x123, x124, s(s(x125)))) ⇒ F(true, s(x123), s(x124), s(x20))≥F(and(gt(s(x123), s(x124)), gt(s(x123), s(x20))), s(x123), s(x124), s(s(x20))))

We simplified constraint (85) using rule (V) (with possible (I) afterwards) using induction on gt(x126, x20)=true which results in the following new constraints:
(87)    (true=true∧s(x122)=s(x128) ⇒ F(true, s(x122), 0, s(0))≥F(and(gt(s(x122), 0), gt(s(x122), s(0))), s(x122), 0, s(s(0))))

(88)    (gt(x129, x130)=true∧s(x122)=s(x129)∧(∀x131:gt(x129, x130)=true∧s(x131)=x129 ⇒ F(true, s(x131), 0, s(x130))≥F(and(gt(s(x131), 0), gt(s(x131), s(x130))), s(x131), 0, s(s(x130)))) ⇒ F(true, s(x122), 0, s(s(x130)))≥F(and(gt(s(x122), 0), gt(s(x122), s(s(x130)))), s(x122), 0, s(s(s(x130)))))

We simplified constraint (87) using rules (I), (II), (IV) which results in the following new constraint:
(89)    (F(true, s(x122), 0, s(0))≥F(and(gt(s(x122), 0), gt(s(x122), s(0))), s(x122), 0, s(s(0))))

We simplified constraint (88) using rules (I), (II), (III), (IV) which results in the following new constraint:
(90)    (gt(x129, x130)=true ⇒ F(true, s(x129), 0, s(s(x130)))≥F(and(gt(s(x129), 0), gt(s(x129), s(s(x130)))), s(x129), 0, s(s(s(x130)))))

We simplified constraint (90) using rule (V) (with possible (I) afterwards) using induction on gt(x129, x130)=true which results in the following new constraints:
(91)    (true=true ⇒ F(true, s(s(x133)), 0, s(s(0)))≥F(and(gt(s(s(x133)), 0), gt(s(s(x133)), s(s(0)))), s(s(x133)), 0, s(s(s(0)))))

(92)    (gt(x134, x135)=true∧(gt(x134, x135)=true ⇒ F(true, s(x134), 0, s(s(x135)))≥F(and(gt(s(x134), 0), gt(s(x134), s(s(x135)))), s(x134), 0, s(s(s(x135))))) ⇒ F(true, s(s(x134)), 0, s(s(s(x135))))≥F(and(gt(s(s(x134)), 0), gt(s(s(x134)), s(s(s(x135))))), s(s(x134)), 0, s(s(s(s(x135))))))

We simplified constraint (91) using rules (I), (II) which results in the following new constraint:
(93)    (F(true, s(s(x133)), 0, s(s(0)))≥F(and(gt(s(s(x133)), 0), gt(s(s(x133)), s(s(0)))), s(s(x133)), 0, s(s(s(0)))))

We simplified constraint (92) using rule (VI) where we applied the induction hypothesis (gt(x134, x135)=true ⇒ F(true, s(x134), 0, s(s(x135)))≥F(and(gt(s(x134), 0), gt(s(x134), s(s(x135)))), s(x134), 0, s(s(s(x135))))) with σ = [ ] which results in the following new constraint:
(94)    (F(true, s(x134), 0, s(s(x135)))≥F(and(gt(s(x134), 0), gt(s(x134), s(s(x135)))), s(x134), 0, s(s(s(x135)))) ⇒ F(true, s(s(x134)), 0, s(s(s(x135))))≥F(and(gt(s(s(x134)), 0), gt(s(s(x134)), s(s(s(x135))))), s(s(x134)), 0, s(s(s(s(x135))))))

We simplified constraint (86) using rule (V) (with possible (I) afterwards) using induction on gt(x136, x20)=true which results in the following new constraints:
(95)    (true=true∧gt(x123, x124)=true∧s(x123)=s(x138)∧(∀x125:gt(x123, x124)=true∧gt(x123, x125)=true ⇒ F(true, x123, x124, s(x125))≥F(and(gt(x123, x124), gt(x123, s(x125))), x123, x124, s(s(x125)))) ⇒ F(true, s(x123), s(x124), s(0))≥F(and(gt(s(x123), s(x124)), gt(s(x123), s(0))), s(x123), s(x124), s(s(0))))

(96)    (gt(x139, x140)=true∧gt(x123, x124)=true∧s(x123)=s(x139)∧(∀x125:gt(x123, x124)=true∧gt(x123, x125)=true ⇒ F(true, x123, x124, s(x125))≥F(and(gt(x123, x124), gt(x123, s(x125))), x123, x124, s(s(x125))))∧(∀x141,x142,x143:gt(x139, x140)=true∧gt(x141, x142)=true∧s(x141)=x139∧(∀x143:gt(x141, x142)=true∧gt(x141, x143)=true ⇒ F(true, x141, x142, s(x143))≥F(and(gt(x141, x142), gt(x141, s(x143))), x141, x142, s(s(x143)))) ⇒ F(true, s(x141), s(x142), s(x140))≥F(and(gt(s(x141), s(x142)), gt(s(x141), s(x140))), s(x141), s(x142), s(s(x140)))) ⇒ F(true, s(x123), s(x124), s(s(x140)))≥F(and(gt(s(x123), s(x124)), gt(s(x123), s(s(x140)))), s(x123), s(x124), s(s(s(x140)))))

We simplified constraint (95) using rules (I), (II), (IV) which results in the following new constraint:
(97)    (gt(x123, x124)=true ⇒ F(true, s(x123), s(x124), s(0))≥F(and(gt(s(x123), s(x124)), gt(s(x123), s(0))), s(x123), s(x124), s(s(0))))

We simplified constraint (96) using rules (I), (II), (III) which results in the following new constraint:
(98)    (gt(x139, x140)=true∧gt(x139, x124)=true∧(∀x125:gt(x139, x124)=true∧gt(x139, x125)=true ⇒ F(true, x139, x124, s(x125))≥F(and(gt(x139, x124), gt(x139, s(x125))), x139, x124, s(s(x125))))∧(∀x141,x142,x143:gt(x139, x140)=true∧gt(x141, x142)=true∧s(x141)=x139∧(∀x143:gt(x141, x142)=true∧gt(x141, x143)=true ⇒ F(true, x141, x142, s(x143))≥F(and(gt(x141, x142), gt(x141, s(x143))), x141, x142, s(s(x143)))) ⇒ F(true, s(x141), s(x142), s(x140))≥F(and(gt(s(x141), s(x142)), gt(s(x141), s(x140))), s(x141), s(x142), s(s(x140)))) ⇒ F(true, s(x139), s(x124), s(s(x140)))≥F(and(gt(s(x139), s(x124)), gt(s(x139), s(s(x140)))), s(x139), s(x124), s(s(s(x140)))))

We simplified constraint (97) using rule (V) (with possible (I) afterwards) using induction on gt(x123, x124)=true which results in the following new constraints:
(99)    (true=true ⇒ F(true, s(s(x145)), s(0), s(0))≥F(and(gt(s(s(x145)), s(0)), gt(s(s(x145)), s(0))), s(s(x145)), s(0), s(s(0))))

(100)    (gt(x146, x147)=true∧(gt(x146, x147)=true ⇒ F(true, s(x146), s(x147), s(0))≥F(and(gt(s(x146), s(x147)), gt(s(x146), s(0))), s(x146), s(x147), s(s(0)))) ⇒ F(true, s(s(x146)), s(s(x147)), s(0))≥F(and(gt(s(s(x146)), s(s(x147))), gt(s(s(x146)), s(0))), s(s(x146)), s(s(x147)), s(s(0))))

We simplified constraint (99) using rules (I), (II) which results in the following new constraint:
(101)    (F(true, s(s(x145)), s(0), s(0))≥F(and(gt(s(s(x145)), s(0)), gt(s(s(x145)), s(0))), s(s(x145)), s(0), s(s(0))))

We simplified constraint (100) using rule (VI) where we applied the induction hypothesis (gt(x146, x147)=true ⇒ F(true, s(x146), s(x147), s(0))≥F(and(gt(s(x146), s(x147)), gt(s(x146), s(0))), s(x146), s(x147), s(s(0)))) with σ = [ ] which results in the following new constraint:
(102)    (F(true, s(x146), s(x147), s(0))≥F(and(gt(s(x146), s(x147)), gt(s(x146), s(0))), s(x146), s(x147), s(s(0))) ⇒ F(true, s(s(x146)), s(s(x147)), s(0))≥F(and(gt(s(s(x146)), s(s(x147))), gt(s(s(x146)), s(0))), s(s(x146)), s(s(x147)), s(s(0))))

We simplified constraint (98) using rule (VI) where we applied the induction hypothesis (∀x125:gt(x139, x124)=true∧gt(x139, x125)=true ⇒ F(true, x139, x124, s(x125))≥F(and(gt(x139, x124), gt(x139, s(x125))), x139, x124, s(s(x125)))) with σ = [x125 / x140] which results in the following new constraint:
(103)    (F(true, x139, x124, s(x140))≥F(and(gt(x139, x124), gt(x139, s(x140))), x139, x124, s(s(x140)))∧(∀x141,x142,x143:gt(x139, x140)=true∧gt(x141, x142)=true∧s(x141)=x139∧(∀x143:gt(x141, x142)=true∧gt(x141, x143)=true ⇒ F(true, x141, x142, s(x143))≥F(and(gt(x141, x142), gt(x141, s(x143))), x141, x142, s(s(x143)))) ⇒ F(true, s(x141), s(x142), s(x140))≥F(and(gt(s(x141), s(x142)), gt(s(x141), s(x140))), s(x141), s(x142), s(s(x140)))) ⇒ F(true, s(x139), s(x124), s(s(x140)))≥F(and(gt(s(x139), s(x124)), gt(s(x139), s(s(x140)))), s(x139), s(x124), s(s(s(x140)))))

We simplified constraint (103) using rule (IV) which results in the following new constraint:
(104)    (F(true, x139, x124, s(x140))≥F(and(gt(x139, x124), gt(x139, s(x140))), x139, x124, s(s(x140))) ⇒ F(true, s(x139), s(x124), s(s(x140)))≥F(and(gt(s(x139), s(x124)), gt(s(x139), s(s(x140)))), s(x139), s(x124), s(s(s(x140)))))

To summarize, we get the following constraints P_≥ for the following pairs.

F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, s(y), z)
- (F(true, s(x29), s(0), 0)≥F(and(gt(s(x29), s(0)), gt(s(x29), 0)), s(x29), s(s(0)), 0))
- (F(true, s(s(x40)), s(0), s(0))≥F(and(gt(s(s(x40)), s(0)), gt(s(s(x40)), s(0))), s(s(x40)), s(s(0)), s(0)))
- (F(true, s(x41), s(0), s(x42))≥F(and(gt(s(x41), s(0)), gt(s(x41), s(x42))), s(x41), s(s(0)), s(x42)) ⇒ F(true, s(s(x41)), s(0), s(s(x42)))≥F(and(gt(s(s(x41)), s(0)), gt(s(s(x41)), s(s(x42)))), s(s(x41)), s(s(0)), s(s(x42))))
- (F(true, s(s(x52)), s(s(0)), 0)≥F(and(gt(s(s(x52)), s(s(0))), gt(s(s(x52)), 0)), s(s(x52)), s(s(s(0))), 0))
- (F(true, s(x53), s(s(x54)), 0)≥F(and(gt(s(x53), s(s(x54))), gt(s(x53), 0)), s(x53), s(s(s(x54))), 0) ⇒ F(true, s(s(x53)), s(s(s(x54))), 0)≥F(and(gt(s(s(x53)), s(s(s(x54)))), gt(s(s(x53)), 0)), s(s(x53)), s(s(s(s(x54)))), 0))
- (F(true, x46, s(x31), x47)≥F(and(gt(x46, s(x31)), gt(x46, x47)), x46, s(s(x31)), x47) ⇒ F(true, s(x46), s(s(x31)), s(x47))≥F(and(gt(s(x46), s(s(x31))), gt(s(x46), s(x47))), s(x46), s(s(s(x31))), s(x47)))
- (F(true, s(x60), 0, s(0))≥F(and(gt(s(x60), 0), gt(s(x60), s(0))), s(x60), s(0), s(0)))
- (F(true, s(s(x71)), 0, s(s(0)))≥F(and(gt(s(s(x71)), 0), gt(s(s(x71)), s(s(0)))), s(s(x71)), s(0), s(s(0))))
- (F(true, s(x72), 0, s(s(x73)))≥F(and(gt(s(x72), 0), gt(s(x72), s(s(x73)))), s(x72), s(0), s(s(x73))) ⇒ F(true, s(s(x72)), 0, s(s(s(x73))))≥F(and(gt(s(s(x72)), 0), gt(s(s(x72)), s(s(s(x73))))), s(s(x72)), s(0), s(s(s(x73)))))
- (F(true, s(s(x83)), s(0), s(0))≥F(and(gt(s(s(x83)), s(0)), gt(s(s(x83)), s(0))), s(s(x83)), s(s(0)), s(0)))
- (F(true, s(x84), s(x85), s(0))≥F(and(gt(s(x84), s(x85)), gt(s(x84), s(0))), s(x84), s(s(x85)), s(0)) ⇒ F(true, s(s(x84)), s(s(x85)), s(0))≥F(and(gt(s(s(x84)), s(s(x85))), gt(s(s(x84)), s(0))), s(s(x84)), s(s(s(x85))), s(0)))
- (F(true, x77, x62, s(x78))≥F(and(gt(x77, x62), gt(x77, s(x78))), x77, s(x62), s(x78)) ⇒ F(true, s(x77), s(x62), s(s(x78)))≥F(and(gt(s(x77), s(x62)), gt(s(x77), s(s(x78)))), s(x77), s(s(x62)), s(s(x78))))
F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, y, s(z))
- (F(true, s(x91), s(0), 0)≥F(and(gt(s(x91), s(0)), gt(s(x91), 0)), s(x91), s(0), s(0)))
- (F(true, s(s(x102)), s(0), s(0))≥F(and(gt(s(s(x102)), s(0)), gt(s(s(x102)), s(0))), s(s(x102)), s(0), s(s(0))))
- (F(true, s(x103), s(0), s(x104))≥F(and(gt(s(x103), s(0)), gt(s(x103), s(x104))), s(x103), s(0), s(s(x104))) ⇒ F(true, s(s(x103)), s(0), s(s(x104)))≥F(and(gt(s(s(x103)), s(0)), gt(s(s(x103)), s(s(x104)))), s(s(x103)), s(0), s(s(s(x104)))))
- (F(true, s(s(x114)), s(s(0)), 0)≥F(and(gt(s(s(x114)), s(s(0))), gt(s(s(x114)), 0)), s(s(x114)), s(s(0)), s(0)))
- (F(true, s(x115), s(s(x116)), 0)≥F(and(gt(s(x115), s(s(x116))), gt(s(x115), 0)), s(x115), s(s(x116)), s(0)) ⇒ F(true, s(s(x115)), s(s(s(x116))), 0)≥F(and(gt(s(s(x115)), s(s(s(x116)))), gt(s(s(x115)), 0)), s(s(x115)), s(s(s(x116))), s(0)))
- (F(true, x108, s(x93), x109)≥F(and(gt(x108, s(x93)), gt(x108, x109)), x108, s(x93), s(x109)) ⇒ F(true, s(x108), s(s(x93)), s(x109))≥F(and(gt(s(x108), s(s(x93))), gt(s(x108), s(x109))), s(x108), s(s(x93)), s(s(x109))))
- (F(true, s(x122), 0, s(0))≥F(and(gt(s(x122), 0), gt(s(x122), s(0))), s(x122), 0, s(s(0))))
- (F(true, s(s(x133)), 0, s(s(0)))≥F(and(gt(s(s(x133)), 0), gt(s(s(x133)), s(s(0)))), s(s(x133)), 0, s(s(s(0)))))
- (F(true, s(x134), 0, s(s(x135)))≥F(and(gt(s(x134), 0), gt(s(x134), s(s(x135)))), s(x134), 0, s(s(s(x135)))) ⇒ F(true, s(s(x134)), 0, s(s(s(x135))))≥F(and(gt(s(s(x134)), 0), gt(s(s(x134)), s(s(s(x135))))), s(s(x134)), 0, s(s(s(s(x135))))))
- (F(true, s(s(x145)), s(0), s(0))≥F(and(gt(s(s(x145)), s(0)), gt(s(s(x145)), s(0))), s(s(x145)), s(0), s(s(0))))
- (F(true, s(x146), s(x147), s(0))≥F(and(gt(s(x146), s(x147)), gt(s(x146), s(0))), s(x146), s(x147), s(s(0))) ⇒ F(true, s(s(x146)), s(s(x147)), s(0))≥F(and(gt(s(s(x146)), s(s(x147))), gt(s(s(x146)), s(0))), s(s(x146)), s(s(x147)), s(s(0))))
- (F(true, x139, x124, s(x140))≥F(and(gt(x139, x124), gt(x139, s(x140))), x139, x124, s(s(x140))) ⇒ F(true, s(x139), s(x124), s(s(x140)))≥F(and(gt(s(x139), s(x124)), gt(s(x139), s(s(x140)))), s(x139), s(x124), s(s(s(x140)))))

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation [18]:

POL(0) = 0
POL(F(x₁, x₂, x₃, x₄)) = -1 - x₁ + x₂ - x₄
POL(and(x₁, x₂)) = 0
POL(c) = -1
POL(false) = 1
POL(gt(x₁, x₂)) = 0
POL(s(x₁)) = 1 + x₁
POL(true) = 0

The following pairs are in P_>:

F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, y, s(z))

The following pairs are in P_bound:

F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, s(y), z)
F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, y, s(z))

The following rules are usable:

false → and(x, false)
x → and(x, true)

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ NonInfProof

                          ↳ QDP

                            ↳ NonInfProof

Q DP problem:
The TRS P consists of the following rules:

F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, s(y), z)

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false

The set Q consists of the following terms:

gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
and(x0, true)
and(x0, false)

We consider the chain F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, s(y), z), F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, s(y), z) which results in the following constraint:
(1)    (F(and(gt(x0, x1), gt(x0, x2)), x0, s(x1), x2)=F(true, x3, x4, x5) ⇒ F(true, x3, x4, x5)≥F(and(gt(x3, x4), gt(x3, x5)), x3, s(x4), x5))

We simplified constraint (1) using rules (I), (II), (III), (VII) which results in the following new constraint:
(2)    (gt(x0, x1)=x24∧gt(x0, x2)=x25∧and(x24, x25)=true ⇒ F(true, x0, s(x1), x2)≥F(and(gt(x0, s(x1)), gt(x0, x2)), x0, s(s(x1)), x2))

We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on and(x24, x25)=true which results in the following new constraint:
(3)    (x26=true∧gt(x0, x1)=x26∧gt(x0, x2)=true ⇒ F(true, x0, s(x1), x2)≥F(and(gt(x0, s(x1)), gt(x0, x2)), x0, s(s(x1)), x2))

We simplified constraint (3) using rule (III) which results in the following new constraint:
(4)    (gt(x0, x1)=true∧gt(x0, x2)=true ⇒ F(true, x0, s(x1), x2)≥F(and(gt(x0, s(x1)), gt(x0, x2)), x0, s(s(x1)), x2))

We simplified constraint (4) using rule (V) (with possible (I) afterwards) using induction on gt(x0, x1)=true which results in the following new constraints:
(5)    (true=true∧gt(s(x29), x2)=true ⇒ F(true, s(x29), s(0), x2)≥F(and(gt(s(x29), s(0)), gt(s(x29), x2)), s(x29), s(s(0)), x2))

(6)    (gt(x30, x31)=true∧gt(s(x30), x2)=true∧(∀x32:gt(x30, x31)=true∧gt(x30, x32)=true ⇒ F(true, x30, s(x31), x32)≥F(and(gt(x30, s(x31)), gt(x30, x32)), x30, s(s(x31)), x32)) ⇒ F(true, s(x30), s(s(x31)), x2)≥F(and(gt(s(x30), s(s(x31))), gt(s(x30), x2)), s(x30), s(s(s(x31))), x2))

We simplified constraint (5) using rules (I), (II), (VII) which results in the following new constraint:
(7)    (s(x29)=x33∧gt(x33, x2)=true ⇒ F(true, s(x29), s(0), x2)≥F(and(gt(s(x29), s(0)), gt(s(x29), x2)), s(x29), s(s(0)), x2))

We simplified constraint (6) using rule (VII) which results in the following new constraint:
(8)    (gt(x30, x31)=true∧s(x30)=x43∧gt(x43, x2)=true∧(∀x32:gt(x30, x31)=true∧gt(x30, x32)=true ⇒ F(true, x30, s(x31), x32)≥F(and(gt(x30, s(x31)), gt(x30, x32)), x30, s(s(x31)), x32)) ⇒ F(true, s(x30), s(s(x31)), x2)≥F(and(gt(s(x30), s(s(x31))), gt(s(x30), x2)), s(x30), s(s(s(x31))), x2))

We simplified constraint (7) using rule (V) (with possible (I) afterwards) using induction on gt(x33, x2)=true which results in the following new constraints:
(9)    (true=true∧s(x29)=s(x35) ⇒ F(true, s(x29), s(0), 0)≥F(and(gt(s(x29), s(0)), gt(s(x29), 0)), s(x29), s(s(0)), 0))

(10)    (gt(x36, x37)=true∧s(x29)=s(x36)∧(∀x38:gt(x36, x37)=true∧s(x38)=x36 ⇒ F(true, s(x38), s(0), x37)≥F(and(gt(s(x38), s(0)), gt(s(x38), x37)), s(x38), s(s(0)), x37)) ⇒ F(true, s(x29), s(0), s(x37))≥F(and(gt(s(x29), s(0)), gt(s(x29), s(x37))), s(x29), s(s(0)), s(x37)))

We simplified constraint (9) using rules (I), (II), (IV) which results in the following new constraint:
(11)    (F(true, s(x29), s(0), 0)≥F(and(gt(s(x29), s(0)), gt(s(x29), 0)), s(x29), s(s(0)), 0))

We simplified constraint (10) using rules (I), (II), (III), (IV) which results in the following new constraint:
(12)    (gt(x36, x37)=true ⇒ F(true, s(x36), s(0), s(x37))≥F(and(gt(s(x36), s(0)), gt(s(x36), s(x37))), s(x36), s(s(0)), s(x37)))

We simplified constraint (12) using rule (V) (with possible (I) afterwards) using induction on gt(x36, x37)=true which results in the following new constraints:
(13)    (true=true ⇒ F(true, s(s(x40)), s(0), s(0))≥F(and(gt(s(s(x40)), s(0)), gt(s(s(x40)), s(0))), s(s(x40)), s(s(0)), s(0)))

(14)    (gt(x41, x42)=true∧(gt(x41, x42)=true ⇒ F(true, s(x41), s(0), s(x42))≥F(and(gt(s(x41), s(0)), gt(s(x41), s(x42))), s(x41), s(s(0)), s(x42))) ⇒ F(true, s(s(x41)), s(0), s(s(x42)))≥F(and(gt(s(s(x41)), s(0)), gt(s(s(x41)), s(s(x42)))), s(s(x41)), s(s(0)), s(s(x42))))

We simplified constraint (13) using rules (I), (II) which results in the following new constraint:
(15)    (F(true, s(s(x40)), s(0), s(0))≥F(and(gt(s(s(x40)), s(0)), gt(s(s(x40)), s(0))), s(s(x40)), s(s(0)), s(0)))

We simplified constraint (14) using rule (VI) where we applied the induction hypothesis (gt(x41, x42)=true ⇒ F(true, s(x41), s(0), s(x42))≥F(and(gt(s(x41), s(0)), gt(s(x41), s(x42))), s(x41), s(s(0)), s(x42))) with σ = [ ] which results in the following new constraint:
(16)    (F(true, s(x41), s(0), s(x42))≥F(and(gt(s(x41), s(0)), gt(s(x41), s(x42))), s(x41), s(s(0)), s(x42)) ⇒ F(true, s(s(x41)), s(0), s(s(x42)))≥F(and(gt(s(s(x41)), s(0)), gt(s(s(x41)), s(s(x42)))), s(s(x41)), s(s(0)), s(s(x42))))

We simplified constraint (8) using rule (V) (with possible (I) afterwards) using induction on gt(x43, x2)=true which results in the following new constraints:
(17)    (true=true∧gt(x30, x31)=true∧s(x30)=s(x45)∧(∀x32:gt(x30, x31)=true∧gt(x30, x32)=true ⇒ F(true, x30, s(x31), x32)≥F(and(gt(x30, s(x31)), gt(x30, x32)), x30, s(s(x31)), x32)) ⇒ F(true, s(x30), s(s(x31)), 0)≥F(and(gt(s(x30), s(s(x31))), gt(s(x30), 0)), s(x30), s(s(s(x31))), 0))

(18)    (gt(x46, x47)=true∧gt(x30, x31)=true∧s(x30)=s(x46)∧(∀x32:gt(x30, x31)=true∧gt(x30, x32)=true ⇒ F(true, x30, s(x31), x32)≥F(and(gt(x30, s(x31)), gt(x30, x32)), x30, s(s(x31)), x32))∧(∀x48,x49,x50:gt(x46, x47)=true∧gt(x48, x49)=true∧s(x48)=x46∧(∀x50:gt(x48, x49)=true∧gt(x48, x50)=true ⇒ F(true, x48, s(x49), x50)≥F(and(gt(x48, s(x49)), gt(x48, x50)), x48, s(s(x49)), x50)) ⇒ F(true, s(x48), s(s(x49)), x47)≥F(and(gt(s(x48), s(s(x49))), gt(s(x48), x47)), s(x48), s(s(s(x49))), x47)) ⇒ F(true, s(x30), s(s(x31)), s(x47))≥F(and(gt(s(x30), s(s(x31))), gt(s(x30), s(x47))), s(x30), s(s(s(x31))), s(x47)))

We simplified constraint (17) using rules (I), (II), (IV) which results in the following new constraint:
(19)    (gt(x30, x31)=true ⇒ F(true, s(x30), s(s(x31)), 0)≥F(and(gt(s(x30), s(s(x31))), gt(s(x30), 0)), s(x30), s(s(s(x31))), 0))

We simplified constraint (18) using rules (I), (II), (III) which results in the following new constraint:
(20)    (gt(x46, x47)=true∧gt(x46, x31)=true∧(∀x32:gt(x46, x31)=true∧gt(x46, x32)=true ⇒ F(true, x46, s(x31), x32)≥F(and(gt(x46, s(x31)), gt(x46, x32)), x46, s(s(x31)), x32))∧(∀x48,x49,x50:gt(x46, x47)=true∧gt(x48, x49)=true∧s(x48)=x46∧(∀x50:gt(x48, x49)=true∧gt(x48, x50)=true ⇒ F(true, x48, s(x49), x50)≥F(and(gt(x48, s(x49)), gt(x48, x50)), x48, s(s(x49)), x50)) ⇒ F(true, s(x48), s(s(x49)), x47)≥F(and(gt(s(x48), s(s(x49))), gt(s(x48), x47)), s(x48), s(s(s(x49))), x47)) ⇒ F(true, s(x46), s(s(x31)), s(x47))≥F(and(gt(s(x46), s(s(x31))), gt(s(x46), s(x47))), s(x46), s(s(s(x31))), s(x47)))

We simplified constraint (19) using rule (V) (with possible (I) afterwards) using induction on gt(x30, x31)=true which results in the following new constraints:
(21)    (true=true ⇒ F(true, s(s(x52)), s(s(0)), 0)≥F(and(gt(s(s(x52)), s(s(0))), gt(s(s(x52)), 0)), s(s(x52)), s(s(s(0))), 0))

(22)    (gt(x53, x54)=true∧(gt(x53, x54)=true ⇒ F(true, s(x53), s(s(x54)), 0)≥F(and(gt(s(x53), s(s(x54))), gt(s(x53), 0)), s(x53), s(s(s(x54))), 0)) ⇒ F(true, s(s(x53)), s(s(s(x54))), 0)≥F(and(gt(s(s(x53)), s(s(s(x54)))), gt(s(s(x53)), 0)), s(s(x53)), s(s(s(s(x54)))), 0))

We simplified constraint (21) using rules (I), (II) which results in the following new constraint:
(23)    (F(true, s(s(x52)), s(s(0)), 0)≥F(and(gt(s(s(x52)), s(s(0))), gt(s(s(x52)), 0)), s(s(x52)), s(s(s(0))), 0))

We simplified constraint (22) using rule (VI) where we applied the induction hypothesis (gt(x53, x54)=true ⇒ F(true, s(x53), s(s(x54)), 0)≥F(and(gt(s(x53), s(s(x54))), gt(s(x53), 0)), s(x53), s(s(s(x54))), 0)) with σ = [ ] which results in the following new constraint:
(24)    (F(true, s(x53), s(s(x54)), 0)≥F(and(gt(s(x53), s(s(x54))), gt(s(x53), 0)), s(x53), s(s(s(x54))), 0) ⇒ F(true, s(s(x53)), s(s(s(x54))), 0)≥F(and(gt(s(s(x53)), s(s(s(x54)))), gt(s(s(x53)), 0)), s(s(x53)), s(s(s(s(x54)))), 0))

We simplified constraint (20) using rule (VI) where we applied the induction hypothesis (∀x32:gt(x46, x31)=true∧gt(x46, x32)=true ⇒ F(true, x46, s(x31), x32)≥F(and(gt(x46, s(x31)), gt(x46, x32)), x46, s(s(x31)), x32)) with σ = [x32 / x47] which results in the following new constraint:
(25)    (F(true, x46, s(x31), x47)≥F(and(gt(x46, s(x31)), gt(x46, x47)), x46, s(s(x31)), x47)∧(∀x48,x49,x50:gt(x46, x47)=true∧gt(x48, x49)=true∧s(x48)=x46∧(∀x50:gt(x48, x49)=true∧gt(x48, x50)=true ⇒ F(true, x48, s(x49), x50)≥F(and(gt(x48, s(x49)), gt(x48, x50)), x48, s(s(x49)), x50)) ⇒ F(true, s(x48), s(s(x49)), x47)≥F(and(gt(s(x48), s(s(x49))), gt(s(x48), x47)), s(x48), s(s(s(x49))), x47)) ⇒ F(true, s(x46), s(s(x31)), s(x47))≥F(and(gt(s(x46), s(s(x31))), gt(s(x46), s(x47))), s(x46), s(s(s(x31))), s(x47)))

We simplified constraint (25) using rule (IV) which results in the following new constraint:
(26)    (F(true, x46, s(x31), x47)≥F(and(gt(x46, s(x31)), gt(x46, x47)), x46, s(s(x31)), x47) ⇒ F(true, s(x46), s(s(x31)), s(x47))≥F(and(gt(s(x46), s(s(x31))), gt(s(x46), s(x47))), s(x46), s(s(s(x31))), s(x47)))

To summarize, we get the following constraints P_≥ for the following pairs.

F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, s(y), z)
- (F(true, s(x29), s(0), 0)≥F(and(gt(s(x29), s(0)), gt(s(x29), 0)), s(x29), s(s(0)), 0))
- (F(true, s(s(x40)), s(0), s(0))≥F(and(gt(s(s(x40)), s(0)), gt(s(s(x40)), s(0))), s(s(x40)), s(s(0)), s(0)))
- (F(true, s(x41), s(0), s(x42))≥F(and(gt(s(x41), s(0)), gt(s(x41), s(x42))), s(x41), s(s(0)), s(x42)) ⇒ F(true, s(s(x41)), s(0), s(s(x42)))≥F(and(gt(s(s(x41)), s(0)), gt(s(s(x41)), s(s(x42)))), s(s(x41)), s(s(0)), s(s(x42))))
- (F(true, s(s(x52)), s(s(0)), 0)≥F(and(gt(s(s(x52)), s(s(0))), gt(s(s(x52)), 0)), s(s(x52)), s(s(s(0))), 0))
- (F(true, s(x53), s(s(x54)), 0)≥F(and(gt(s(x53), s(s(x54))), gt(s(x53), 0)), s(x53), s(s(s(x54))), 0) ⇒ F(true, s(s(x53)), s(s(s(x54))), 0)≥F(and(gt(s(s(x53)), s(s(s(x54)))), gt(s(s(x53)), 0)), s(s(x53)), s(s(s(s(x54)))), 0))
- (F(true, x46, s(x31), x47)≥F(and(gt(x46, s(x31)), gt(x46, x47)), x46, s(s(x31)), x47) ⇒ F(true, s(x46), s(s(x31)), s(x47))≥F(and(gt(s(x46), s(s(x31))), gt(s(x46), s(x47))), s(x46), s(s(s(x31))), s(x47)))

POL(0) = 0
POL(F(x₁, x₂, x₃, x₄)) = -1 - x₁ + x₂ - x₃ + x₄
POL(and(x₁, x₂)) = 0
POL(c) = -1
POL(false) = 1
POL(gt(x₁, x₂)) = 0
POL(s(x₁)) = 1 + x₁
POL(true) = 0

The following pairs are in P_>:

F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, s(y), z)

The following pairs are in P_bound:

F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, s(y), z)

The following rules are usable:

false → and(x, false)
x → and(x, true)

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ NonInfProof

                          ↳ QDP

                            ↳ NonInfProof

                              ↳ QDP

                                ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false

The set Q consists of the following terms:

gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
and(x0, true)
and(x0, false)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.